
DISCH
CONJUNCT1
CONJUNCT2
ASSUME
CONJ
MP

Goal 

p /\ q ==> q /\ p




----------------  ----------------
p /\ q |- p /\ q  p /\ q |- p /\ q
----------------  -----------------
p /\ q |- q        p /\ q |- p
-------------------------------- CONJ
p /\ q |- q /\ p
---------------------- DISCH
|- p /\ q ==> q /\ p

let thm1 = ASSUME `p /\ q`
let thm2 = CONJUNCT1 thm1
let thm3 = CONJUNCT2 thm1
let thm4 = CONJ thm3 thm2
let thm5 = DISCH `p /\ q` thm4




Goal

(p ==> q ==> r) ==> p ==> q ==> r




                                --------------------
                                  p /\ q |- p /\ q
-------------------------------  ------------------   ----------------
p ==> q ==> r |- p ==> q ==> r   p /\ q |- p          p /\ q |- p /\ q 
---------------------------------------------      ------------
p ==> q ==> r, p /\ q |- q ==> r                   p /\ q |- q
-----------------------------------------------------------------
p ==> q ==> r, p /\ q |- r
----------------------------------
p ==> q ==> r |- p /\ q ==> r
----------------------------------
(p ==> q ==> r) ==> p /\ q ==> r

DISCH
ASSUME
MP
CONJUNCT1
CONJUNCT2

(p ==> q ==> r) ==> p /\ q ==> r

let pqr = ASSUME `p ==> q ==> r`
let pq = ASSUME `p /\ q`
let p = CONJUNCT1 pq
let q = CONJUNCT2 pq
let qr = MP pqr p
let r = MP qr q
let thm1 = DISCH `p /\ q` r
let thm2 = DISCH `p ==> q ==> r` thm1

g `(!x. (x < 1)) \/ (!x:num. ?y. x = y)`;;
b()
e DISJ2_TAC
e STRIP_TAC
e (EXISTS_TAC `x:num`)
e (REFL_TAC);;


1;;



      
  --------------------------
    p ==> q, q ==> r, p |- r
----------------------------------------
|- (p ==> q) ==> (q ==> r) ==> p ==> r`

\H: p==>q. \H1: q==>r. \H2: p. H1 (H H2)

DISCH `p ==> q` 
 (DISCH `q ==> r` 
  (DISCH `p:bool`
    (MP (ASSUME `q ==> r`) (MP (ASSUME `p ==> q`) (ASSUME `p:bool`)))))


g `p /\ (q \/ r) ==> (p /\ q) \/ (p /\ r)`;;
b();;
p();;

let thm5 = prove(`p /\ (q \/ r) ==> (p /\ q) \/ (p /\ r)`,
  DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC DISJ_CASES_TAC) THENL
  [DISJ1_TAC; DISJ2_TAC] THEN CONJ_TAC THEN FIRST_ASSUM ACCEPT_TAC
);;

let thm6 = prove(`p ==> (~p ==> q)`,
  DISCH_TAC THEN
  DISCH_THEN (fun pf -> FIRST_ASSUM (fun p -> CONTR_TAC (MP (NOT_ELIM pf) p)))
);;



NOT
  
CONTR_TAC



p();;
DISJ
